Termination Proof Script

• Consider the SCC {22}. There are no usable rules. By taking the AF π with π(FIRST) = 1 together with the lexicographic path order with empty precedence, rule 22 is strictly decreasing.


• Consider the SCC {23}. There are no usable rules. The constraints could not be solved.


• Consider the SCC {21}. There are no usable rules. By taking the AF π with π(SEL) = 1 together with the lexicographic path order with empty precedence, rule 21 is strictly decreasing.


• Consider the SCC {24,25,30,31}. There are no usable rules. By taking the AF π with π(QUOTE) = π(s) = 1 and π(sel) = π(SEL1) = 2 together with the lexicographic path order with empty precedence, the rules in {30,31} are weakly decreasing and the rules in {24,25} are strictly decreasing. There is one new SCC.
  • Consider the SCC {30}. By taking the AF π with π(QUOTE) = 1 together with the lexicographic path order with empty precedence, rule 30 is strictly decreasing.


• Consider the SCC {27}. There are no usable rules. By taking the AF π with π(FIRST1) = 1 together with the lexicographic path order with empty precedence, rule 27 is strictly decreasing.


• Consider the SCC {29}. There are no usable rules. By taking the AF π with π(QUOTE1) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 29 is strictly decreasing.


• Consider the SCC {33}. There are no usable rules. By taking the AF π with π(UNQUOTE) = 1 together with the lexicographic path order with empty precedence, rule 33 is strictly decreasing.


• Consider the SCC {36}. There are no usable rules. By taking the AF π with π(UNQUOTE1) = 1 and π(cons1) = [2] together with the lexicographic path order with empty precedence, rule 36 is strictly decreasing.